Nuprl Definition : ma-single-effect0
0,22
postcript
pdf
ma-single-effect0(
x
;
A
;
k
;
T
;
f
)
== with declarations
==
ds:
x
:
A
==
da:
k
:
T
==
effect of
k
(v) is
x
:=
s
,
v
.
f
(
s
(
x
),
v
) s v
latex
Definitions
with declarations ds:
ds
da:
da
effect of
k
(v) is
x
:=
f
s v
,
x
:
v
,
x
.
A
(
x
)
,
f
(
a
)
FDL editor aliases
ma-single-effect0
origin
s,v. f(s(x),v) s v s,v. f(s(x),v) s v x.A(x)